i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), snd:msg-spec(ds;da), es:ES, l:IdLnk.
source(l) = i  @i[[A;snd]]  Prop 

latex

Definitions

x:A. B(x), isrcv(e), b, P  Q, s = t, left+right, P  Q, valtype(e), kind(e), loc(e), <a,b>, S  T, state@i, Type, x.A(x), x. t(x), nil, IdLnkDeq, product-deq(A;B;a;b), {x:A| B(x) }, Atom$n, ecl(ds;da), msg-spec(ds;da), ES, P & Q, es-decls(es;i;ds;da), source(l), es-init(es;e), E, Prop, Top, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, rec(x.A(x)), action[[a n]][e1;e2], , S  T, f(a), mapfilter(f;P;L), msg-item(ds;da;k;l), IdDeq, vartype(i;x), ecl-tags(l;snd), tag(e), (x  l), lnk(e), val(e), (state when e), tagged-list-messages(s;v;L), with decls ds dasends on l from e include f(e) and only these for tags in tgs, {T}, P  Q, @i[[x;snd]], Void, 2of(t), rcv(l,tg), KindDeq, f(x)?z, type List, 1of(t), Valtype(da;k), x:AB(x), State(ds), , x:AB(x), Id, IdLnk, Knd, a:A fp B(a), t  T, @i state ds, SQType(T), s ~ t

Lemmas

subtype rel dep function, subtype rel self, Id sq, es-state-type-implies, lsrc wf, event system wf, msg-spec wf, ecl wf, fpf wf, es-decls wf, es-decls-iff, es-sends-iff wf, tagged-list-messages wf, es-state-when wf, es-val wf, es-lnk wf, l member wf, es-tag wf, ecl-tags wf, es-vartype wf, id-deq wf, mapfilter wf, es-bact wf, top wf, es-E wf, es-init wf, es-loc-init, product-deq wf, idlnk-deq wf, Id wf, nat wf, decl-state wf, pi1 wf, fpf-cap wf, Kind-deq wf, rcv wf, pi2 wf, Knd wf, IdLnk wf, es-state wf, es-loc wf, es-valtype wf, ma-valtype wf, es-kind wf, assert wf, es-isrcv wf